|
In theoretical computer science, in particular in automated theorem proving and term rewriting, a binary relation (→) on the set of terms is called a rewrite relation if it is closed under contextual embedding and under instantiation; formally: if ''l''→''r'' implies ''u''(HREF="http://www.kotoba.ne.jp/word/11/Substitution (logic)#First-order logic" TITLE="Substitution (logic)#First-order logic">σ )''p''→''u''()''p'' for all terms ''l'', ''r'', ''u'', each path ''p'' of ''u'', and each substitution σ. If (→) is also irreflexive and transitive, then it is called a rewrite ordering,〔Dershowitz, Jouannaud (1990), sect.2.1, p.251〕 or rewrite preorder. If the latter (→) is moreover well-founded, it is called a reduction ordering,〔Dershowitz, Jouannaud (1990), sect.5.1, p.270〕 or a reduction preorder. Given a binary relation ''R'', its rewrite closure is the smallest rewrite relation containing ''R''.〔Dershowitz, Jouannaud (1990), sect.2.2, p.252〕 A transitive and reflexive rewrite relation that contains the subterm ordering is called a simplification ordering.〔Dershowitz, Jouannaud (1990), sect.5.2, p.274〕 ==Properties== * The converse, the symmetric closure, the reflexive closure, and the transitive closure of a rewrite relation is again a rewrite relation, as are the union and the intersection of two rewrite relations.〔Dershowitz, Jouannaud (1990), sect.2.1, p.251〕 * The converse of a rewrite order is again a rewrite order. * While rewrite orders exist that are total on the set of ground terms ("ground-total" for short), no rewrite order can be total on the set of all terms.〔Since ''x''<''y'' implies ''y''<''x'', since the latter is an instance of the former, for variables ''x'', ''y''.〕〔Dershowitz, Jouannaud (1990), sect.5.1, p.272〕 * A term rewriting system is terminating if its rules are subset of a reduction ordering.〔i.e. if ''l''''i'' > ''r''''i'' for all ''i'', where (>) is a reduction ordering; the system needn't have finitely many rules〕〔 * Conversely, for every terminating term rewriting system, the transitive closure of (::=) is a reduction ordering,〔 which needn't be extendable to a ground-total one, however. For example, the ground term rewriting system is terminating, but can be shown so using a reduction ordering only if the constants ''a'' and ''b'' are incomparable.〔Since e.g. ''a''>''b'' implied ''g(''a'')>''g''(''b''), meaning the second rewrite rule was not decreasing.〕〔Dershowitz, Jouannaud (1990), sect.5.1, p.271〕 * A ground-total and well-founded rewrite ordering〔i.e. a ground-total reduction ordering〕 necessarily contains the proper subterm relation on ground terms. * Conversely, a rewrite ordering that contains the subterm relation〔i.e. a simplification ordering〕 is necessarily well-founded, when the set of function symbols is finite.〔〔The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.〕 * A finite term rewriting system is terminating if its rules are subset of the strict part of a simplification ordering.〔〔 Here: p.287; the notions are named slightly different.〕 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「rewrite order」の詳細全文を読む スポンサード リンク
|